(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 607
Accept states: [608, 609, 610, 611]
Transitions:
607→608[twoto_1|0]
607→609[twice_1|0]
607→610[p_1|0]
607→611[0_1|0]
607→607[s_1|0]
607→612[s_1|1]
607→637[s_1|1]
607→614[s_1|2]
607→639[s_1|2]
607→616[twoto_1|2]
607→641[s_1|2]
607→643[s_1|2]
607→645[twice_1|2]
612→613[p_1|1]
613→614[s_1|1]
613→616[twoto_1|2]
614→615[p_1|1]
615→616[twoto_1|1]
616→617[s_1|1]
616→623[s_1|2]
616→627[twice_1|2]
617→618[s_1|1]
617→622[p_1|2]
618→619[s_1|1]
618→621[p_1|2]
619→620[p_1|1]
620→621[p_1|1]
621→622[p_1|1]
622→623[s_1|1]
622→627[twice_1|2]
623→624[s_1|1]
623→626[p_1|2]
624→625[p_1|1]
625→626[p_1|1]
626→627[twice_1|1]
627→628[s_1|1]
627→634[s_1|2]
627→617[s_1|2]
627→623[s_1|3, s_1|2]
627→627[twice_1|3, twice_1|2]
628→629[s_1|1]
628→633[p_1|2]
629→630[s_1|1]
629→632[p_1|2]
630→631[p_1|1]
631→632[p_1|1]
632→633[p_1|1]
633→634[s_1|1]
633→617[s_1|2]
633→623[s_1|2]
633→627[twice_1|2, twice_1|3]
634→635[s_1|1]
634→608[p_1|2]
634→616[p_1|2]
635→636[p_1|1]
636→608[p_1|1]
636→616[p_1|1]
637→638[p_1|1]
638→639[s_1|1]
638→641[s_1|2]
638→643[s_1|2]
638→645[twice_1|2]
639→640[p_1|1]
640→641[s_1|1]
640→643[s_1|2]
640→645[twice_1|2]
641→642[p_1|1]
642→643[s_1|1]
642→645[twice_1|2]
643→644[p_1|1]
644→645[twice_1|1]
645→646[s_1|1]
646→647[s_1|1]
646→609[s_1|2]
646→645[s_1|2]
647→648[s_1|1]
647→654[p_1|2]
648→649[s_1|1]
648→653[p_1|2]
649→650[s_1|1]
649→652[p_1|2]
650→651[p_1|1]
651→652[p_1|1]
652→653[p_1|1]
653→654[p_1|1]
654→609[s_1|1]
654→645[s_1|1]